\documentclass[10pt]{article}
\usepackage{mathpartir}
\usepackage{amsmath}
\usepackage{amssymb}

\usepackage{xifthen}

\usepackage{hyperref}

\usepackage{tgpagella}
\usepackage{mathpazo}

\newcommand{\Sequent}[2]{\ensuremath{#1 \vdash #2}}
\newcommand{\Numeric}[1]{\ensuremath{\operatorname{numeric}(#1)}}
\newcommand{\Keyword}[1]{\ensuremath{\mathsf{#1}}}

% Macros for BNF-ish abstract syntax
\newcommand{\SynClassAndCase}[2]{#1 &\mathbin{::=} & #2 \\}
\newcommand{\SynCase}[1]{& \mathbin{|} & #1 \\}
\newenvironment{Syntax}
  {
      $$
      \begin{array}{lcl}
  }
  {
      \end{array}
      $$
  }

% macros for Petr4 syntax
\newcommand{\Error}{\Keyword{error}}
\newcommand{\Void}{\Keyword{void}}
\newcommand{\Bool}{\Keyword{bool}}
\newcommand{\True}{\Keyword{true}}
\newcommand{\False}{\Keyword{false}}
\newcommand{\String}{\Keyword{string}}
\newcommand{\Varbit}[1]{\Keyword{varbit}\langle#1\rangle}
\newcommand{\Int}[1]{
    \Keyword{int}
    \ifthenelse{\equal{#1}{}}
        {}
        {\langle #1 \rangle}
}
\newcommand{\Bit}[1]{\Keyword{bit}\langle#1\rangle}
\newcommand{\Stack}[2]{#1\,\Keyword{stack}\langle#2\rangle}
\newcommand{\Set}[1]{#1\,\Keyword{set}}
\newcommand{\Prod}{\times}
\newcommand{\Arrow}{\longrightarrow}
\newcommand{\TApp}[2]{#1 \langle #2 \rangle}
\newcommand{\SignedLit}[2]{#1\Keyword{s}#2}
\newcommand{\UnsignedLit}[2]{#1\Keyword{w}#2}
\newcommand{\Member}{.}
\newcommand{\Index}[2]{#1 [#2]}
\newcommand{\Slice}[3]{#1 [#2 : #3]}
\newcommand{\SetLit}[1]{\{#1\}}
\newcommand{\Many}[1]{\overline{#1}}
\newcommand{\Uop}{\ominus}
\newcommand{\Binop}{\odot}
\newcommand{\Cast}[2]{(#1)#2}
\newcommand{\Ternary}[3]{#1 \mathbin{?} #2 \mathbin{:} #3}
\newcommand{\AppWithTypes}[3]{
    #1
    \ifthenelse{\equal{#2}{}}
        {}
        {\langle #2 \rangle}
    (#3)
}
\newcommand{\FunApp}[3]{\AppWithTypes{#1}{#2}{#3}}
\newcommand{\Mask}{\mathbin{\&\&\&}}
\newcommand{\Range}{\mathbin{..}}
\newcommand{\Header}[2]{\Keyword{header}\ #1\ \{ #2 \}}
\newcommand{\HeaderUnion}[2]{\Keyword{header\_union}\ #1\ \{ #2 \}}
\newcommand{\Struct}[2]{\Keyword{struct}\ #1\ \{ #2 \}}
\newcommand{\ErrorDecl}[1]{\Error.f : \Error}
\newcommand{\Enum}[2]{\Keyword{enum}\ #1\ \{ #2 \}}
\newcommand{\SEnum}[2]{\Keyword{enum}\ #1\ \{ #2 \}}
\newcommand{\Extern}[3]{
    \Keyword{extern}\ #1
    \ifthenelse{\equal{#2}{}}
        {}
        {\langle #2 \rangle}\ \{ #3 \}
}
\newcommand{\Newtype}[2]{\Keyword{newtype}\ #1\ #2}
\newcommand{\Control}[3]{\Keyword{control}\ \AppWithTypes{#1}{#2}{#3}}
\newcommand{\Package}[3]{\Keyword{package}\ \AppWithTypes{#1}{#2}{#3}}
\newcommand{\Parser}[3]{\Keyword{parser}\ \AppWithTypes{#1}{#2}{#3}}

\newcommand{\Typed}[3]{\Sequent{#1;#2}{#3}}
\newcommand{\Var}{\Keyword{Var}}
\newcommand{\Str}{\Keyword{Str}}
\newcommand{\Name}{\Keyword{Name}}
\newcommand{\Z}{\mathbb{Z}}

\newcommand{\Lookup}[2]{\operatorname{\Keyword{lookup}} #1\,#2}

\newcommand{\Spec}{https://p4.org/p4-spec/docs/P4-16-v1.1.0-spec.html}
\newcommand{\SpecRef}[1]{
    \footnote{\url{\Spec\##1}}
}

\begin{document}

Variables \(x, y \in \Var\).

Type names \(T \in \Name\). Both type variables and names of things like headers
are represented by type names.

Field names \(f \in \Name\).

Integer literals \(m, n \in \Z\).

String literals \(s \in \Str\).

Unary operators \(\ominus \in \{\dots\}\).

Binary operators \(\odot \in \{\dots\}\).

Expression types.
\begin{Syntax}
    \SynClassAndCase{\tau}{\Bool}
    \SynCase{\Error}
    \SynCase{\Int{}}
    \SynCase{\Int{n}}
    \SynCase{\Bit{n}}
    \SynCase{\Varbit{n}}
    \SynCase{.T}
    \SynCase{T}
    \SynCase{\TApp{T}{\Many{\tau}}}
    \SynCase{\Stack{T}{n}}
    \SynCase{\tau_1 \Prod \cdots \Prod \tau_n}
    \SynCase{\Void}
    \SynCase{\Set{\tau}}
\end{Syntax}

Some of these types are not permitted in the surface syntax. For example, you
cannot use \(\Set{\tau}\) types directly, but you can create expressions of type
\(\Set{\tau}\).\SpecRef{sec-set-exprs}

Expressions.
\begin{Syntax}
    \SynClassAndCase{e}{\True}
    \SynCase{\False}
    \SynCase{n}
    \SynCase{\SignedLit{m}{n}}
    \SynCase{\UnsignedLit{m}{n}}
    \SynCase{s}
    \SynCase{x}
    \SynCase{\Member f}
    \SynCase{\Index{e_1}{e_2}}
    \SynCase{\Slice{e_1}{e_2}{e_3}}
    \SynCase{\SetLit{\Many{e}}}
    \SynCase{\Uop e}
    \SynCase{e_1 \Binop e_2}
    \SynCase{\Cast{\tau}{e}}
    \SynCase{\tau \Member f}
    \SynCase{\Error \Member f}
    \SynCase{\Ternary{e_1}{e_2}{e_3}}
    \SynCase{\FunApp{e}{\Many{\tau}}{\Many{e}}}
    \SynCase{\FunApp{e}{}{\Many{e}}}
    \SynCase{e_1 \Mask e_2}
    \SynCase{e_1 \Range e_2}
\end{Syntax}

Directions for function arguments.
\begin{Syntax}
    \SynClassAndCase{p}{\Keyword{in}}
    \SynCase{\Keyword{out}}
    \SynCase{\Keyword{inout}}
\end{Syntax}

Method declarations.
\begin{Syntax}
    \SynClassAndCase{m}{\Keyword{constructor}\ \FunApp{T}{}{\Many{x : \tau\, p}}}
    \SynCase{\FunApp{T}{\Many{T}}{\Many{x : \tau\, p}}}
\end{Syntax}

Declarations.
\begin{Syntax}
    \SynClassAndCase{D}{\Header{T}{\Many{f: \tau}}}
    \SynCase{\HeaderUnion{T}{\Many{f: \tau}}}
    \SynCase{\Struct{T}{\Many{f: \tau}}}
    \SynCase{\ErrorDecl{T}}
    \SynCase{\Enum{T}{\Many{f}}}
    \SynCase{\SEnum{T}{\Many{f: e}}}
    \SynCase{\Extern{T}{\Many{T}}{\Many{m}}}
    \SynCase{\Newtype{T}{\tau}}
    \SynCase{\Control{T}{\Many{T}}{\Many{x : \tau\,p}}}
    \SynCase{\Parser{T}{\Many{T}}{\Many{x : \tau\,p}}}
    \SynCase{\Package{T}{\Many{T}}{\Many{x : \tau\,p}}}
\end{Syntax}

Type contexts are lists \(\Gamma = \Gamma_1, \dots, \Gamma_n\) of scopes
\(\Gamma_n\). Each scope is a list \(\Gamma_i = x_1 : \tau_1, \dots, x_n
: \tau_n\). There is a function \(\Lookup{\Gamma}{x}\) which finds the first
binding for \(x\) in the context \(\Gamma\).

Declaration contexts are lists of declarations \(\Delta = D_1, \dots, D_n\).
TODO: There is a well-formedness condition here, I think?

The typing judgment for expressions takes the form \(\Typed{\Delta}{\Gamma}{e
: \tau}\) and is defined by the following rules.
\[
    \inferrule{\Lookup{\Gamma}{x} = \tau}{\Typed{\Delta}{\Gamma}{x : \tau}}
\]

\end{document}
